% Section~\ref{s:why-immutability} presents a case for introducing immutability into a language.

\section{How Can We Improve on the State of the Art?}
\label{s:immutability-future}

The two major improvements achieved by the immutability proposals of the last decade are: (1) support for \textit{transitive} read-only by supporting the enforcement of not just the reference to an object but also any further references from such object being read-only and (2) support for \textit{object immutability} rather than just read-only references thus guaranteeing that no unexpected \textit{alias} to an immutable object can change its state. Javari~\cite{TschantzE2005} supports the former, while \Joe~\cite{oestlund:2008:oui} and OIGJ~\cite{zibin:2010:oigj} support both.

To achieve read-only references, Javari utilizes additional
annotations on any variable declaration in Java
(e.g. \texttt{readonly}) that is then checked by the type system
to guarantee that no read-only reference is assigned to or
modified. Javari's implementation in Java is available for
download\footnote{\url{http://types.cs.washington.edu/javari/}}.

\Joe utilizes an ownership-based type system and a very simple effect
system which keeps track of which object is modified and prevents
any modifications to objects which are \textit{immutable} or
\textit{read-only}. A
Polyglot-based\footnote{\url{http://www.cs.cornell.edu/projects/polyglot/}}
prototype implementation is available.

OIGJ makes use of Java's generic types
to allow the types to state whether the object is
\textit{mutable} or \textit{immutable} when creating the
object. OIGJ also supports \textit{read-only} types. A
Checker-Framework-based\footnote{\url{http://types.cs.washington.edu/checker-framework/}}
prototype implementation is available.

This section presents examples taken from three recent
immutability proposals by the authors.
Subsection~\ref{s:cases-from-javari} presents enforcement of
contracts and read-only access to internal data in the Javari
system~\cite{TschantzE2005} which supports read-only
references. Subsection~\ref{s:cases-from-oigj} presents a larger
example similar to \code{LinkedList} from the Java collections
written in the OIGJ~\cite{zibin:2010:oigj} system supporting both
read-only references and object immutability, among other
features. Subsection~\ref{s:cases-from-joe} shows how to support
flexible lists and context-based read-only in
\Joe~\cite{oestlund:2008:oui}, a system supporting object
immutability and more. Both OIGJ and \Joe make use of
\textit{ownership}~\cite{clarke:1998:ownership-types-for-flexible-alias-protection}
to be able to properly support deep immutability as discussed later in
this chapter. Please refer to Figure~\ref{fig:features}
%% MDE: There are no page references in version submitted for review.
% on page~\pageref{fig:features}
for a
summary of supported features in the abovementioned systems and
several others.

%% Alex: These probably needs to be merged into one coherent motivation, rather than per-proposal as it is now.

\subsection{Cases from Javari}
\label{s:cases-from-javari}

This subsection shows examples of read-only as found in the Javari
system.

\paragraph{Enforcement of contracts}

Consider a voting system containing the following routine:
%
\begin{java}
ElectionResults tabulate(Ballots votes) { ... }
\end{java}
%
In order to permit verification (e.g. double checking) of the results,
it is necessary to safeguard the integrity of
the ballots.  This requires a machine-checked guarantee that
the routine does not modify its input \jv{votes}.
Using Javari, the specification of \jv{tabulate} could declare that
\jv{votes} is read-only:
%
\begin{java}
ElectionResults tabulate(readonly Ballots votes) { 
  ^($\cdots$)^  // ^(cannot tamper with the votes)^
}
\end{java}
%
and the compiler ensures that implementers of \jv{tabulate} do
not violate the contract.  


\paragraph{Read-only access to internal data}

Accessor methods often return data that already exists as part of
the representation of the module.  

For example, consider the  \jv{Class.getSigners} method, which returns the
entities that have digitally signed a particular implementation.
In JDK 1.1.1, its implementation is simple and efficient:

% \begin{verbatimfont}
% \begin{verbatim}
\begin{java}
  class Class {
    private Object[] signers;
    Object[] getSigners() { 
      return signers;
    }
  }
\end{java}
% \end{verbatim}
% \end{verbatimfont}

\noindent
This is a security hole, because a malicious client can call
\jv{getSigners} and then add elements to the
\jv{signers} array.

Javari permits the following solution:

% \newcommand{\sqbr}{\jv{[]}}
% \begin{verbatimfont}
% \begin{Verbatim}[commandchars=\|\[\],commentchar=\!]
%   class Class {
%     private Object|sqbr[] signers;
%     |underline[readonly] Object|sqbr[] getSigners() { 
%       return signers;
%     }
%   }
% \end{Verbatim}
% \end{verbatimfont}

\begin{java}
  class Class {
    private Object[] signers;
    readonly Object[] getSigners() { 
      return signers;
    }
  }
\end{java}

The \readonly{} keyword ensures that the caller of
\jv{Class.get\-Signers} cannot modify the returned array, thus
permitting the simple and efficient implementation of the method to
remain in place without exposing the representation to undesired
changes.\footnote{The returned array is aliased by the \mytt{signers}
  field, so \jv{Class} code can still change it even if external code
  cannot.  The specification of \jv{getSigners} does not state the
  desired semantics in this case, so this is an acceptable implementation.
  If a different semantics were desired, the method specification could note
  that the returned reference reflects changes to the signers of the
  \jv{Class}; alternately, the method specification, or an external
  analysis, might require that the result is used before the next
  modification of \jv{signers}.}

An alternate solution to the \jv{getSigners} problem, which was actually
implemented in later versions of the JDK, is to return a copy of the array
\mytt{signers}~\cite{Bloch2001}.
This works, but is expensive.  
For example, a file system may allow a client read-only access to its contents:

% \begin{verbatimfont}
% \begin{Verbatim}[commandchars=\|\[\],commentchar=\!]
\begin{java}
  class FileSystem {
    private List<Inode> inodes;
    List<Inode> getInodes() {
      ^($\cdots$)^ // ^(Unrealistic to copy)^
    }
  }
\end{java}
% \end{Verbatim}
% \end{verbatimfont}

\noindent
Javari allows the programmer to avoid the high cost of
copying \jv{inodes} by writing the return type of the method as:

% \begin{verbatimfont}
% \begin{Verbatim}[commandchars=\|\[\],commentchar=\!]
%     |underline[readonly] List<|underline[readonly] Inode> getInodes()
% \end{Verbatim}
% \end{verbatimfont}

\begin{java}
  readonly List<readonly Inode> getInodes()
\end{java}

\noindent This return type prevents the \jv{List} or any of its
contents from being modified by the client.
As with all parameterized classes, the client specifies the
type argument, including whether it is read-only or not, 
independently of the parameterized typed. 

In this case, the list returned is declared to be read-only and
contain read-only elements, and, thus, a client of \jv{getInodes} is
unable to modify the list or its elements.


\subsection{Cases from OIGJ}
\label{s:cases-from-oigj}

Figure~\ref{f:OIGJ-LinkedList} shows an implementation of \code{LinkedList} in OIGJ that follows closely the Sun's implementation but does not contain any additional bounds checking and supporting code that would prevent it from fitting on one page.
We explain this example in three stages:
    (i)~we first explain the data-structure, i.e.,
        the fields of a list and its entries (lines~\ref{Entry:start}--\ref{OIGJ:header}),
    (ii)~then we discuss the \textit{raw} constructors that enable the creation of
        immutable lists (lines~\ref{OIGJ:Raw:ctor1}--\ref{OIGJ:Raw:end}),
        and
    (iii)~finally we dive into the complexities of inner classes and iterators
        (lines~\ref{OIGJ:iterator}--\ref{I:Iterator:end}). Note that method guards~\cite{HuangZS2007:cJ} state that the method is only applicable if the type variable matches the bound stated by the guard (e.g. method \code{next} inside the \code{ListItr} can only be called if \code{ItrI} is a subtype of \code{Mutable}).


\begin{figure}
\begin{java}
class Entry<O,I,E> { ^( \label{Entry:start} )^
  E element;
  Entry<O,I,E> next, prev; ^( \label{Entry:next} )^
} ^( \label{Entry:end} )^
class LinkedList<O,I,E> { ^( \label{OIGJ:LinkedList} )^
  Entry<This,I,E> header; ^( \label{OIGJ:header} )^
  <I extends Raw>? LinkedList() { ^( \label{OIGJ:Raw:ctor1} )^
    this.header = new Entry<This,I,E>(); ^( \label{OIGJ:Raw:I1} )^
    header.next = header.prev = header; ^( \label{OIGJ:assignment:ctor1} )^
  }
  <I extends Raw>? LinkedList(Collection<?,ReadOnly,E> c) { ^(\label{OIGJ:Raw:ctor2} )^
    this();  this.addAll(c); ^( \label{OIGJ:call-ctor1} )^
  }
  <I extends Raw>? void addAll(Collection<?,ReadOnly,E> c) { ^(\label{OIGJ:addAll:definition} )^
    Entry<This,I,E> succ = this.header, pred = succ.prev; ^(\label{OIGJ:Raw:I2} )^
    for (E e : c) {
      Entry<This,I,E> en=new Entry<This,I,E>();
      en.element=e; en.next=succ; en.prev=pred;
      pred.next = en;  pred = en;  } ^(\label{OIGJ:assignment:addAll} )^
    succ.prev = pred; ^(\label{OIGJ:assignment:addAll:prev} )^
  } ^( \label{OIGJ:Raw:end} )^
  int size() {^($\cdots$)^} ^( \label{OIGJ:size} )^
  <ItrI extends ReadOnly> Iterator<O,ItrI,I,E> iterator() { ^(\label{OIGJ:iterator} )^
    return this.new ListItr<ItrI>(); ^(\label{ListItr:create} )^
  }
  void remove(Entry<This,Mutable,E> e) {
    e.prev.next = e.next; ^(\label{ListItr:prev} )^
    e.next.prev = e.prev; ^(\label{ListItr:prev2} )^
  }
  class ListItr<ItrI> implements Iterator<O,ItrI,I,E> { ^(\label{ListItr:start} \label{ListItr:Iterator} )^
    Entry<This,I,E> current; ^(\label{OIGJ:assignable} )^
    <ItrI extends Raw>? ListItr() { ^(\label{ListItr:ctor} )^
      this.current = LinkedList.this.header; ^(\label{ListItr:ctor-assignment} )^
    }
    <ItrI extends Mutable>? E next() { ^(\label{ListItr:next} )^
      this.current = this.current.next; ^(\label{ListItr:next-assignment} )^
      return this.current.element;
    }
    <I extends Mutable>? void remove() { ^(\label{ListItr:remove} )^
      LinkedList.this.remove(this.current); ^(\label{ListItr:remove-call} )^
    }
} } ^( \label{ListItr:end} )^
interface Iterator<O,ItrI,CollectionI,E> {  ^( \label{I:Iterator} )^
  boolean hasNext(); ^( \label{I:hasNext} )^
  <ItrI extends Mutable>? E next(); ^( \label{I:next} )^
  <CollectionI extends Mutable>? void remove(); ^( \label{I:remove} )^
} ^( \label{I:Iterator:end} )^
\end{java}
\caption{\code{LinkedList<O,I,E>} in OIGJ\@.}
%todo{Add declaration, at least, for \code{Entry} constructor.}
%we now use the default ctor defined by Java that initialize everything to 0/null
\label{f:OIGJ-LinkedList}
\end{figure}


\paragraph{LinkedList data-structure}
A linked list has a header field (line~\ref{OIGJ:header})
    pointing to the first entry.
Each entry has an \code{element} and
    pointers to the \code{next} and \code{prev} entries (line~\ref{Entry:next}).
We explain first the immutability and then the ownership of each field.

Note that we assume that \code{O} refers to the current class instance owner and \code{I} or \code{ItrI} refer to the appropriate current immutability that is either class instance or method call specific.

An (im)mutable list contains (im)mutable entries,
    i.e., the entire data-structure is either mutable or immutable as a whole.
Hence, all the fields have the same immutability \code{I}.
The underlying generic type system propagates the immutability information
    without the need for special typing rules.

Next consider the ownership of the fields of \code{LinkedList} and \code{Entry}.
\code{This} on line~\ref{OIGJ:header} expresses that the
    reference \code{header} points to an \code{Entry} owned by \this,
    i.e., the entry is encapsulated and
    cannot be aliased outside of \this.
\code{O} on line~\ref{Entry:next} expresses that
    the owner of \code{next} is the same as the owner of the entry,
    i.e., a linked-list owns \emph{all} its entries.
Note how the generics mechanism propagates the owner parameter,
    e.g., the type of \code{this.header.next.next} is \code{Entry<\underline{This},I,E>}.
Thus, the owner of all entries is the \this{} object, i.e., the list.
OIGJ provides \textit{deep ownership} or \textit{owners-as-dominators}
guarantees as discussed in another chapter~\cite{ClarkeOSWChapter}.
%in this book~\cite{AliasingBook}.

Finally, note that the field \code{element} has no immutability nor owner parameters,
    because they will be specified by the client that instantiates the list type,
    e.g., \\
    \code{LinkedList<This,Mutable,Date<\underline{World,ReadOnly}>>}


\paragraph{Immutable object creation}
A constructor that is making an immutable object must be able to set the fields of the object.
It is not acceptable to mark such constructors as \Mutable,
    which would permit arbitrary side effects, possibly including making mutable aliases to \code{this}.
OIGJ uses a fourth kind of immutability,~\textit{raw},
    to permit constructors to perform limited side effects without
    permitting modification of immutable objects.
Phrased differently,
\code{Raw} represents a partially-initialized \emph{raw}
    object that can still be arbitrarily mutated, but after
    it is cooked (fully initialized), then the object might become immutable.
The constructors on lines~\ref{OIGJ:Raw:ctor1} and~\ref{OIGJ:Raw:ctor2}
    are guarded with \code{Raw}, and therefore
    can create both mutable and immutable lists.

Objects must not be captured in their raw state to prevent further mutation after the object is cooked.
If a programmer could declare a field, such as \code{Date\hgn{O,Raw}},
    then a raw date could be stored there, and later it could be used to mutate a cooked immutable date.
Therefore, a programmer can write the \code{Raw} type only after the \code{extends} keyword, but
    \emph{not} in any other way.
As a consequence, in a \code{Raw} constructor, \this{} can only escape as \code{ReadOnly}.

An object becomes \emph{cooked} either
    when its new expression (construction) finishes executing
    or when its owner is \emph{cooked}.
The entries of the list (line~\ref{OIGJ:header}) are \this-owned.
Indeed, the entries are mutated after their constructor has finished, but before their owner (list) is cooked,
    on lines~\ref{OIGJ:assignment:ctor1}, \ref{OIGJ:assignment:addAll}, and \ref{OIGJ:assignment:addAll:prev}.
This shows the power of combining immutability and ownership:
    we are able to create immutable lists \emph{only} by using the fact that the list owns its entries.
If those entries were \emph{not} owned by the list, then this mutation of entries might be visible
    to the outside world, thus breaking the guarantee that an immutable object never changes.
By enforcing ownership, OIGJ ensures that such illegal mutations cannot occur.

OIGJ requires that all access and assignment to a \this-owned field
    must be done via \this.
For example, see \code{header}, on lines~\ref{OIGJ:Raw:I1},~\ref{OIGJ:assignment:ctor1},~\ref{OIGJ:Raw:I2},
    and~\ref{ListItr:ctor-assignment}.
In contrast, fields \code{next} and \code{prev} (which are not \this-owned)
    do not have such a restriction,
    as can be seen on lines~\ref{ListItr:prev}--\ref{ListItr:prev2}.
    Note that inner classes are treated differently, and are
    allowed to access the outer object's \this-owned fields. This
    arguably gives a more flexible system, which for instance
    allows the iterator class in the example, but at the cost of
    less clear containment properties.

\paragraph{Iterator implementation and inner classes}
An \emph{iterator} has an underlying \emph{collection}, and the immutability
    of these two objects might be different.
For example, you can have
\begin{itemize}\itemsep 0pt \parskip 0pt
\item
    a mutable iterator over a mutable collection
    (the iterator supports both \code{remove()} and \code{next()}),
\item
    a mutable iterator over a readonly/immutable collection
    (the iterator supports \code{next()} but not \code{remove()}), or
\item
    a readonly iterator over a mutable collection
    (the iterator supports \code{remove()} but not \code{next()},
    which can be useful if you want to pass an iterator to a method that may not advance the iterator but may remove the current element).
\end{itemize}

Consider the \code{Iterator<O,ItrI,CollectionI,E>} interface
    defined on lines~\ref{I:Iterator}--\ref{I:Iterator:end},
    and used on lines~\ref{OIGJ:iterator} and~\ref{ListItr:Iterator}.
\code{ItrI} is the iterator's immutability, whereas
    \code{CollectionI} is intended to be the underlying collection's immutability
    (see on line~\ref{ListItr:Iterator} how the collection's immutability \code{I} is used in the place of \code{CollectionI}).
Line~\ref{I:next} requires a mutable \code{ItrI} to call \code{next()},
    and line~\ref{I:remove} requires a mutable \code{CollectionI} to call \code{remove()}.

Inner class \code{ListItr} (lines~\ref{ListItr:start}--\ref{ListItr:end})
    is the implementation of \code{Iterator} for list.
Its full name is \code{LinkedList<O,I,E>.List\-Itr<ItrI>},
    and on line~\ref{ListItr:start} it extends \code{Iterator<O,ItrI,I,E>}.
It reuses the owner parameter \code{\underline{O}} from \code{LinkedList},
    but declares a new immutability parameter \code{\underline{ItrI}}.
An inner class, such as \code{ListItr<ItrI>}, only declares an immutability parameter
    because it inherits the owner parameter from its outer class.
\code{ListItr} and \code{LinkedList} have the same owner~\code{O},
    but different immutability parameters (\code{ItrI} for \code{ListItr}, and \code{I} for \code{LinkedList}).
\code{ListItr} must inherit \code{LinkedList}'s owner because it directly accesses the (\this-owned)
    representation of \code{LinkedList} (line~\ref{ListItr:ctor-assignment}),
    which would be illegal if their owner was different.
For example, consider the types of \code{this} and \code{LinkedList.this}
    on line~\ref{ListItr:ctor-assignment}:
%
\begin{java}
Iterator<O,ItrI,^($\cdots$)^> thisIterator = this;
LinkedList<O,I,^($\cdots$)^> thisList = LinkedList.this;
\end{java}
%
Because line~\ref{ListItr:ctor} sets the bound of~\code{ItrI} to be \code{Raw},
    \this{} can be mutated.  By contrast, the bound of \code{I} is \code{ReadOnly}, so
\code{LinkedList.this} cannot.

Finally, consider the creation of a new \emph{inner} object on line~\ref{ListItr:create}
    using \code{\underline{this}.new ListItr<ItrI>()}.
This expression is type-checked both as a method call (whose receiver is \this)
    and as a constructor call.
Observe that the bound of \code{ItrI} is \code{ReadOnly} (line~\ref{OIGJ:iterator})
    and the guard on the constructor is \code{Raw} (line~\ref{ListItr:ctor}),
    which is legal because a \code{Raw} constructor can create both mutable and immutable objects.


\subsection{Cases from \Joe}
\label{s:cases-from-joe}

This subsection presents a different take on how to specify
read-only and immutability, in which the context where an object
is used determines its mutability properties.


\paragraph{A short note on effects}

\Joe employs a very simple effects system to specify what a class
or method will mutate. The effects are specified in terms of
contexts (or owners) inspired by
\textsf{Joe}$_1$~\cite{clarke:2002:disjoint}. In \Joe context
parameters are decorated with modes which govern how objects
belonging to a particular context may be treated.


\paragraph{Separating Mutability of List and its Contents}

Figure \ref{fig:list-class-one} shows part of an implementation of
a list class. The class is parameterized over permissions
(\code{data} in this case) which specify that the list has
privilege to reference objects in that context. The parameter
\code{data} is decorated with the mode read-only (denoted
`\Read{}'), indicating that the list will never cause write
effects to objects owned by \code{data}.  The owner of the list is
called \code{owner} and is implicitly declared. The method
\code{getFirst()} is annotated with \code{revoke owner}, which
means that the method will not modify the list or its transitive
state. This means the same as if \code{owner-} and \code{this-}
would have appeared in the class header. This allows the method to
be called from objects where the list owner is read-only. Finally,
\code{strictlyoutside} means that the \code{data} context must not
be the same context as the \code{owner} of the list.
%
\begin{figure}
\begin{small}
\begin{java}
class Link<data- strictlyoutside owner> {
  data:Object obj = null;
  owner:Link<data> next = null;  
}

class List<data- strictlyoutside owner> {
  this:Link<data> first = null;
  void addFirst(data:Object obj) {
    this:Link<data> tmp = new this:Link<data>();
    tmp.obj = obj;
    tmp.next = this.first;
    this.first = tmp;
  }
  void filter(data:Object obj) {
    this:Link<data> tmp = this.first;
    if (tmp == null) return;
    while (tmp.next != null)
      if (tmp.next.obj == obj)
        tmp.next = tmp.next.next;
      else
        tmp = tmp.next;
    if (this.first != null && this.first.obj == obj)
      this.first = this.first.next;
  }
  data:Object getFirst() revoke owner { return this.first.obj; } 
}
\end{java}
\end{small}
\caption{Fragment of a list class. As the \texttt{data} owner
  parameter is declared read-only (via `\Read{}') in the class
  header, no method in \texttt{List} may modify an object owned by
  \texttt{data}.  Observe that the syntactic overhead is minimal
  for an ownership types system.}
\label{fig:list-class-one}
\end{figure}

This list class can be instantiated in four different ways,
depending on the access rights to the owners in the type held by
the current context:
%
\begin{itemize}
\item both the list and its data objects are immutable, which
  only allows \code{getFirst()} to be invoked, and its resulting
  object is immutable;
\item both are mutable, which imposes no restrictions;
\item the list is mutable but the data objects are not, which
  imposes no additional restrictions, \code{getFirst()} returns
  a read-only reference; and
\item the data objects are mutable, but the list not, which
  only allows \code{getFirst()} to be invoked, and the resulting
  object is mutable. 
\end{itemize}
%
The last form is interesting and relies on the fact that it is
known, courtesy of ownership types, that the data objects are not
part of the representation of the list. Without this distinction
one could easily create an example where a mutable alias can be
returned from a read-only object.


\subsection{Complementing Immutability}
\label{s:complementing-immutability}

In this subsection we explain why blindly adding immutability support
to any OO language with aliasing might not be such a good
idea and how it can be addressed by careful
application of various ownership techniques discussed in the rest
of this book.

Boyland~\cite{Boy06} criticizes existing proposals for handling
read-only references on the following points:

\begin{enumerate}
\item Read-only references can be aliased, for example by capturing a method argument;
\item A read-only annotation does not express whether 
  \begin{enumerate}
  \item the referenced \emph{object} is immutable, so the
    referent is known to never change;
  \item a read-only reference is unique and thus effectively immutable;
  \item mutable aliases of a read-only reference can exist,
    which makes possible
    \emph{observational exposure}, which occurs when changes to state
    are observed through a read-only reference.
  \end{enumerate}
\end{enumerate}

\noindent
Essentially, Boyland is criticizing reference immutability for not being
object immutability.  In some contexts, object immutability is more useful,
and in other contexts, reference immutability is more useful.  Furthermore,
as we noted earlier, different contexts require other differences (such as
representation immutability for reasoning about the memory system, and
abstract immutability for reasoning about client code semantics).
Boyland's criticisms can be addressed, for those contexts where object
immutability is desired, by augmenting reference immutability with object
immutability.

For example, \Joe addresses all of these problems. First, \Joe
supports owner-polymorphic methods, which can express that a
method does not capture one or more of its arguments. Second,
owners are decorated with modes that govern how the objects owned
by that owner will be treated in a particular context. Together
with auxiliary constructs inherited from
\Joline~\cite{wrigstad:2006:phd}, the modes can express
immutability both in terms of 2.a) and 2.b), and read-only which
permits the existence of mutable aliases (2.c). Moreover, \Joe
supports fractional permissions~\cite{Boy03} --- converting a
mutable unique reference into several immutable references for a
certain context. This allows safe representation exposure without
the risk for observational exposure.

OIGJ and \Joe allow both read-only references and immutable objects
in the same language. This provides the safety desired by
Boyland's second point, but also allows coding patterns which do
rely on observing changes in an object. In order to support such
flexibility it appears necessary to employ some kind of
\emph{alias control} mechanism, which in the cases of OIGJ and
\Joe is ownership.


\subsubsection{Ownership and Immutability}

Ownership
types~\cite{clarke:1998:ownership-types-for-flexible-alias-protection,clad-thesis}
impose a structure on the references between objects in the
program heap. Languages with ownership, such as for instance
\Joline~\cite{wrigstad:2006:phd} and OGJ~\cite{PotaninNCB2006},
prevent aliasing to the internal state of an object. While
preventing exposure of owned objects, ownership does not address
exposing immutable parts of an object which cannot break
encapsulation, even though the idea was originally sprung out of a
proposal supporting that~\cite{noble:1998:flap}.

One possible application of ownership types is the ability to
reason about read and write effects~\cite{ClarkD2002} which has
complimentary goals to object immutability.
Universes~\cite{DietlM2005} is a Java language extension combining
ownership and read-only references.  Most ownership systems
enforce that all reference chains to an owned object pass through
the owner.  Universes relaxes this requirement by enforcing this
rule only for mutable references, i.e., read-only references may
be shared without restriction.

Universes, OIGJ, and \Joe provide what we call context-based
immutability. Here it is possible to create a writable list with
writable elements and pass it to some other context where the
elements are read-only. This other context may add elements to the
list (or reorder them) but not mutate the elements, while the
original creator of the list does not lose the right to mutate the
elements.

A read-only reference to an object does not preclude the existence
of mutable references to the same object elsewhere in the system.
This allows observational exposure~\cite{Boy06} --- for good and
evil. Object immutability imposes all restrictions of a read-only
reference, but also guarantees that no aliases with write
permission exist in the system. One simple way of creating an
immutable object is to move a \emph{unique} reference into a
variable with immutable
type~\cite{boyapati-thesis,oestlund:2008:oui}.

%%% Local Variables: 
%%% TeX-command-default: "PDF"
%%% End: 
